COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	outline basic structure
C00003 ENDMK
C⊗;
outline basic structure

  details
   input/output
    cnf
   format of clause
    p-lists and macros

 strategies
  choice
  editing

   rules of inference
    res, par, demod, unit-red
   tricks
    standardize
    subsumption
    unify

******************************
languages for t.p.
    wos-overbeek-..

  on-line
   current features
    simple manipulations
    naming
    matching
    inferencing
     res-par-simp
    sub-proofs

   current "interesting" features
    SEt
    FIND

  weaknesses
    US-PR-EX  and instantiation

 programmable
  what is needed